$\forall$$A$:Type, ${\it eq}$:EqDecider($A$), ${\it ds}$:fpf($A$; $x$.Type), $x$:$A$.
\\[0ex]subtype\_rel(fpf{-}cap(${\it ds}$; ${\it eq}$; $x$; void); fpf{-}cap(${\it ds}$; ${\it eq}$; $x$; top))